\documentclass[orivec]{llncs}

\usepackage{headers}
\usepackage{macro}



%opening
\title{Systemic approach for toxicity analysis}
\author{Cinzia Di Giusto   \and Hanna Klaudel \and Franck Delaplace}
\institute{Université d'Evry - Val d'Essonne, Laboratoire IBISC, Evry, France}

\begin{document}


\maketitle

\begin{abstract}
A high-level Petri net framework is introduced for the toxic risk assessment 
in biological and bio-synthetic systems.
Unlike empirical techniques mostly used in toxicology or toxicogenomics, we propose 
a systemic approach consisting of a series of behavioral rules (reactions) that depend on abstract discrete ``expression'' levels of involved agents (species). 
We introduce a finite state high-level Petri net model allowing exhaustive verification (model-checking) of properties related to equilibrium alteration or appearing of hazardous behaviors.
The approach is applied to the study of the impact of the aspartame assimilation into the blood glucose regulation process.
\end{abstract}
 
\section{Introduction}
    %% DEFINITION ET DOMAINE
Toxicology~\cite{Waters2004} studies the adverse effects of the exposures to chemicals at various levels of living entities: organism, tissue, cell or intracellular molecular systems. During the last decade, the accumulation of genomic and post-genomic data together with the introduction of new technologies for gene analysis has opened the way to  \emph{toxicogenomics}. Toxicogenomics combines toxicology with 
``Omics'' technologies\footnote{“Omics” technologies are methodologies such as genomics, transcriptomics, proteomics and metabolomics.} 
to study the \emph{mode-of-action} of toxicants or environmental stressors on biological systems.
The mode-of-action is understood as the sequence of events from the absorption of chemicals to a toxic outcome.
Toxicogenomics potentially improves clinical diagnosis capabilities and facilitates the identification of potential toxicity  in drug discovery~\cite{Foster2007} or in the design of bio-synthetic entities~\cite{synthetic}. \looseness=-1

%% OBJECTIFS
The main approach used in toxicogenomics employs empirical analysis like in   the identification of molecular biomarkers, \ie indicators of disease or toxicity in the form of specific gene expression patterns~\cite{DeCristofaro2008}.
Clearly, biomarkers remain observational indicators linking genes related measures to toxic states. In this proposal, we complement these empirical methods with a computational technique  that aims at discovering the molecular mechanisms of toxicity. 
This  way, instead of studying the  phenomenology of the toxic impacts, we focus on the processes triggering adverse effects on organisms. 
Usually, the toxicity process  is defined as a sequence of physiological events that causes the abnormal behavior of a living organism  with respect to its healthy state.
Healthy physiological states generally correspond to homeostasis, namely a process that maintains a dynamic stability of internal conditions against changes in the external environment. 
Hence, we will consider toxicity outcomes as deregulation of homeostasis processes, namely deviation of some intrinsic referential equilibrium  of the system. \looseness=-1

Biological processes are usually given in terms of pathways which are  causal chains of the responses to stimuli, this way the deregulation of homeostasis  appears as the  activation or inhibition of  unexpected but existing pathways. Moreover, 
in the context of toxicogenomics it is crucial to take into account at least two other parameters: the exposure time  and the thresholds dosage delimiting the ranges of safe and hazardous effects.  

In this paper, we  depict and analyze the mechanistic process of toxicology using high-level Petri nets. 
Our work is inspired  by the definition of  reaction systems as given  in \cite{DBLP:journals/ijfcs/BrijderEMR11}. 
 A reaction system is a set of \emph{reactions}, each of them defined as a triple $(R, I, P)$ where $R$ is the set of reactants, $I$ the set of inhibitors and $P$ the set of products, and $R,I$ and $P$ are taken from a common set of species \res. Reaction systems are based on three foundational principles: 
 \begin{enumerate}[1.]
 \item \label{item:react} a reaction can take place only if all the reactants involved are available but none of the inhibitors is; 
 \item \label{item:quantity} if a species is available then a sufficient amount of it is present to trigger a reaction; \looseness=-1
 \item species are not persistent: they become unavailable if they are not sustained by a reaction.
\end{enumerate}
From this model we retain the idea of reactions but we significantly change the semantics. 
 The first change concerns principle \ref{item:quantity}: species are available at a given discrete abstract  level. This is mainly related to the need of expressing toxicants doses. The corresponding  discretization is built observing thresholds levels in dose-response curves. 
The second and more fundamental change regards the introduction of discrete time constraints. Time plays a role in the evolution of species, more precisely, species are associated to a decay time $\delta$, meaning that their  level diminishes with time.  This accounts for the presence of a non-specified environment that consumes and degrades species, thus allowing to abstract away from reactions that may be neglected in the specified context.
Each reaction $(R, I, P)$ is extended with   levels for all its reactants and inhibitors.  Reactions  can take place only if each reactant is present at least at a given level and each involved inhibitor is at a level strictly inferior to the given one. As a result, the  level of products of the reaction can be increased or decreased.

Summing up, systems are build out of  a series of behavioral reactions among involved agents or species.  
We model such systems into  high-level Petri nets and  apply it to toxicogenomics problems, namely deregulation of homeostatic processes.
Toxicity questions are expressed using a suitable temporal logic like CTL \cite{emerson}. By observing that our modeling has a finite state space, it is therefore natural to address the satisfiability of these formulae using classic verification techniques such as model checking. 


We apply the modeling and verification process on the example of blood glucose regulation in human body showing the maintenance of the homeostasis. In particular, we highlight how the interplay between the assimilation of aspartame and glucose regulation causes the appearance of unwanted behaviors.

{\bf Organization of the paper.} 
 The paper is organized as follows:  Section \ref{sec:petri} recalls basic definitions and notations on high-level Petri nets. Next, Section \ref{sec:example} describes our running example of blood glucose regulation. Section \ref{sec:reaction} introduces the principles behind reaction networks and  presents their high-level Petri net modeling. Then Section \ref{sec:toxic} shows how to check toxicology properties and finally, Section \ref{sec:concl} concludes with some considerations on future work. \looseness=-1
% 



\section{Preliminaries}\label{sec:petri}
We recall here the general notations together with some elements of  the semantics of high-level Petri nets \cite{DBLP:series/eatcs/Jensen92}.
\begin{definition}%[high-level Petri nets]
\label{def:PTS}
A \emph{high-level Petri net} $N$ is a tuple $(Q, T, F, L, M_0)$ where:
\begin{itemize}
 \item $Q$ is the set of places,

 \item $T$ is the set of transitions and $Q \cap T = \emptyset$;

 \item $F \subseteq (Q \times T) \cup (T \times Q)$ is the set of arcs; 
 \item $L$ is the labeling function from places $Q$, transitions $T$ and arcs $F$   to  a set of labels defined as follows:
\renewcommand{\labelitemii}{$-$} 
\begin{itemize}
 \item $\forall q \in Q$, $L(q) $ is the type of $q$, \ie a (possibly infinite) set or Cartesian product of sets of integer values;
 \item $\forall t \in T$, $L(t)$ is a  computable boolean expression  with variables and integer values; 
 \item and $\forall f\in F$, $L(f)$  is a  tuple of variables and integer values compatible with the adjacent place.  
\end{itemize}
 \item $M_0$ is the initial marking which associates to each place  $q \in Q$ a multiset of tokens in $L(q)$.
\end{itemize} 
\end{definition}

Observe that we are considering a subclass of high-level Petri nets where at most one arc per direction  for each pair place/transition   is allowed and only one token can flow through. 
The behavior of high-level Petri nets is defined as usual: markings are functions from places in $Q$ to multisets of possibly structured tokens in $L(q)$ and a transition $t \in T$ is \emph{enabled} at  marking $M$, if there exists an evaluation $\sigma$ of all variables in the labeling of $t$  such that the guard $L(t)$ evaluates to true ($L_{\sigma}(t) = \mathsf{true}$) and there are enough tokens in all input places $q$ to satisfy the corresponding input arcs, \ie $L_{\sigma}((q,t)) \in M(q)$.
% and all input arc labels are $ \qquad \forall q \in \pre{t},   [L((q,t))]_{\sigma} \in M(q),$$
%where $\pre{t} =\{q\in Q \mid (q,t) \in F\}$ denotes the set of input places of a transition $t$. 
Then, the firing of $t$ produces the marking $M'$:  
$$\forall q \in Q, M'(q) = M(q) - L_{\sigma}((q,t)) + L_{\sigma}((t,q)). $$
with $L_{\sigma}(f) = 0 $ if $f\notin F$, $-$ and $ +$ are  multiset  operators for removal and adding of one element, respectively. We denote it by $\firing{M}{t}{\sigma}{M'}$. 

By convention, primed version of variables (e.g. $x'$) are used to annotate  output arcs of transitions, their evaluation is  possibly computed using unprimed variables (e.g. $x$ and $y$) appearing on input arcs. With an abuse of notation, singleton markings are denoted without brackets, the same is used in  arc annotations. An example of firing is shown in  Figure \ref{fig:exfiring}. 
We say that a marking $M$ is \emph{reachable} from the initial marking $M_0$ if there exists a firing sequence $(t_1, \sigma_1), \dots, (t_n, \sigma_n)$ such that 
 $\firing{M_0}{t_1}{\sigma_1}{M_1} \dots \firing{M_{n-1}}{t_n}{\sigma_n}{M}$.



 \begin{figure}[t]
\centering
\subfigure[Before the firing\label{fig:before}]{
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

% \tikzstyle{place}=[circle,thick,draw=blue!75,fill=blue!30,minimum size=7mm]
% \tikzstyle{transition}=[rectangle,thick,draw=black!75,
% 			 fill=black!20,minimum size=4mm]
 \tikzstyle{every token}=[font=\small]

  \node [place, label = left: $q_1$] at (0,1.5) (Q1){$7$};
  \node [place, label=left:$q_2$]at (0,-1.5)  (Q2){$5$};
  \node [place, label = right: $q_3$] at (1.5,0) (Q3){};
  
  \node [transition] (t) [  label={[red] left:$\begin{array}{lc}
                                                &x>y ~\wedge \\ &x'=x+y
                                               \end{array}$}] at (0,0) {$t$}
   edge [pre]    node[right] {$x$}    (Q1)
   edge [pre]    node[right] {$y$}    (Q2)
   edge [post]   node[above]{$x'$}    (Q3);
\end{tikzpicture}} \quad
\subfigure[After the firing \label{fig:after}]{
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

 %\tikzstyle{place}=[circle,draw,fill=blue!20,minimum size=7mm]
 %\tikzstyle{transition}=[rectangle,thick,draw=black!75,
 		%	 fill=black!20,minimum size=4mm]
 \tikzstyle{every token}=[font=\small]

  \node [place, label = left: $q_1$] at (0,1.5) (Q1){};
  \node [place, label=left:$q_2$]at (0,-1.5)  (Q2){};
  \node [place, label = right: $q_3$] at (1.5,0) (Q3){12};
  
  \node [transition] (t) [  label={[red] left:$\begin{array}{lc}
                                                &x>y ~\wedge \\ &x'=x+y
                                               \end{array}$}] at (0,0) {$t$}
   edge [pre]    node[right] {$x$}    (Q1)
   edge [pre]    node[right] {$y$}    (Q2)
   edge [post]   node[above]{$x'$}    (Q3);
\end{tikzpicture}}
\caption{Example of firing with $\sigma = \{ x= 7, y=5, x'=12\}$.} \label{fig:exfiring}
\end{figure}
 


\section{Blood glucose regulation}\label{sec:example}
Here we introduce our running example:  \emph{glucose regulation} in human body (Figure \ref{fig:glucose}). %as it is a familiar process and it shows that our model is not limited to genetic regulations but it may express other kinds of interactions. 
In the following, we are always referring to the process under normal circumstances in a healthy body.

Glucose regulation is a homeostatic process: \ie the rates of glucose in blood (\emph{glycemia}) must remain stable at what we call the equilibrium state. 
Glycemia is regulated by  two hormones: \emph{insulin} and  \emph{glucagon}. When glycemia rises (for instance as a result of the digestion of a meal), insulin  promotes the storing of glucose in muscles through the  glycogenesis process, thus decreasing the blood glucose levels. 
Conversely, when glycemia is critically low, glucagon  stimulates the process of glycogenolysis that increases the blood glucose level by transforming glycogen back into glucose.

 \begin{figure}[b]
\centering
\includegraphics[width=0.5\textwidth]{glucose.pdf} 
\caption{Glucose metabolism} \label{fig:glucose}
\end{figure}

We will focus on the assimilation of sweeteners: \ie sugars  or  artificial sweeteners such as aspartame. Whenever we eat something sweet either natural or artificial, the sweet sensation sends a signal to the brain (through \emph{neurotransmitters}) that in turns stimulates the production of insulin by pancreas. In the case of sugar, the digestion transforms food into nutrients (\ie glucose) that are absorbed by blood.
This way, sugar through digestion  increases glucose in blood giving the sensation of satiety. In case the income of glucose produces hyperglycemia,  the levels of glucose are promptly equilibrated by the intervention of insulin.
Unlike sugar, artificial sweeteners are not assimilated by the body, hence they do not increase the glucose levels in blood. Nevertheless  the insulin produced under the stimuli originated by the sweet sensation, although weak, can still cause the rate of glucose to drop engendering hypoglycemia. In response to that, the brain induces the  stimulus of \emph{hunger}. As a matter of fact this appears as an unwanted/toxic behavior, indeed the assimilation of food (even if it contains aspartame) should calm hunger and induce satiety not the opposite. 

This schema suggests that we should consider four  levels for glycemia: low, hunger, equilibrium and high. Likewise for insulin we assume three levels: inactive, low and high. All other actors involved in glucose regulation, have only two  levels (inactive or active).  
%In this example, concerning the durations of reactions, all complementary ones such as production of insulin and glucagon,  take the same amount of time, the signal to the brain is the fastest, and the decay of  glycemia values are much longer than the digestion process. 
In the following sections, we will see how to model the glucose metabolism and how to verify the unexpected behaviors of artificial sweeteners.


\section{Petri net modeling}\label{sec:reaction}
A reaction network is  composed of a set of species $\res$ governed by a set of reactions $\RS$.
We begin by giving some intuitions on  their  dynamics.

% \comment{remove figure}
% 
% \begin{figure}[t]
% \centering
% \includegraphics[width=0.7\textwidth]{decay.pdf}
%  \caption{Figure (a) depicts an example of degradation function that is discretized in Figure (b) into three levels (0,1 and 2) } \label{fig:decay}
% \end{figure}

Species in  \res represent the actors of the modeled system. In the example introduced above, we have concrete species such as aspartame and also more abstract ones representing ratios or concepts like glycemia. 
Species may have several \emph{expression} levels. Levels are determined  
by the observable behavior of  species,  \ie  they refer to a change in the capability of action of species. In toxicology, they may   represent dosages. We assume,  for each species $s$, an arbitrary but finite number  $\setlev_s$ of levels, and each $s$ is initialized at a certain  level $\level{s}$. For certain species, we assume the presence of a non specified environment that acts on them by decreasing gradually their expression levels. This special activity is called \emph{decay} and is modeled by various durations associated  to expression levels. Decay may be  unbounded indicating that the level of the species can only change by result of a reaction.
%, so the environment has no effect on the species.  
 It is formalized by  a function that associates to each level  either $\omega$ (unbounded) or its finite duration:  
$$\life_s:[0..\setlev_s-1] \to \nat^+ \cup \{\omega \}.$$
For all species $s\in\res$ we require that $\life_s(0) = \omega $ meaning that the duration of the basal level must be unbounded.


\begin{example}[Glucose metabolism -- species]\label{ex:glucose}
Take the example from Section \ref{sec:example}.
The set of involved species is $$\res = \{ Sugar, Aspartame, Glycemia, Glucagon, Insulin\}$$ and their expression levels and  corresponding decays are:
$$ 
\begin{array}{|lcl|}
\hline
  \mbox{levels} & \hspace{2cm} & \mbox{durations} \\
	\hline
	\setlev_{sugar}=\{0,1\} && \life_{sugar}(1)=2 \\
	\hline
  \setlev_{aspartame}=\{0,1\} && \life_{aspartame}(1)=2 \\
	\hline
  \setlev_{glycemia}=\{0,1,2,3\} \quad && \life_{glycemia}(1)=8 \\
  && \life_{glycemia}(2)=8\\
  && \life_{glycemia}(3)=8\\
	\hline
  \setlev_{glucagon}=\{0,1\} && \life_{glucagon}(1)=3\\
	\hline
  \setlev_{insulin}=\{0,1,2\} && \life_{insulin}(1)=3\\
  && \life_{insulin}(2)=3\\
	\hline
\end{array}
$$
 The levels of glycemia are: 0 corresponding to low, 1 to hunger, 2 to equilibrium and 3 to high. Likewise for insulin we have 0 that corresponds to inactive, 1 to low and 2 to high. All levels for the other species are 0 for inactive and 1 for active.
\hfill $\diamond$
 \end{example} 




The evolution of species $s\in\res$ is governed by a set of reactions  \RS, each being of the form: \looseness=-1
\begin{equation}\label{eq:reaction}
\rho ::= \tuple{R_{\rho}, I_{\rho}, P_{\rho}}
%\tuple{(r_j, \level{j})_{j \in R}, (i_h, \level{h})_{h\in I}, (p_k, op)_{k \in P} }, 
\end{equation}
 where $R_{\rho}$ (reactants), $I_{\rho}$ (inhibitors) are sets of pairs $(s, \level{s})$ and $P_{\rho}$ (products) is a non empty set of pairs $(s, z)$, where $\level{s} \in [0..\setlev_s-1]$ and $z  \in \mathbb{Z}$.
 Species can appear at most once in each set $R_{\rho}$, $I_{\rho}$ and $P_{\rho}$. They can be present in both $R_{\rho}$ and $I_{\rho}$ but they must occur with different levels\footnote{Observe that a species can appear in the same reaction as reactant at level $\level{r}$, inhibitor at level $\level{i} > \level{r}$ and product.}. %$+$ defines increase and $-$ decrease of levels of products. 
We write $s \in R_{\rho}$ to denote  $(s, \cdot) \in R_{\rho}$ similarly for $I_{\rho}$ and $P_{\rho}$ and we omit index $\rho$ if it is clear from the context ($\rho = \tuple{R,I,P}$).

%For instance (from Example \ref{ex:glucose}) we have reaction $\rho_7 = \tuple{\{(Insulin,1)\},\{ (Glycemia,2)\}, \{(Glycemia,-)\}}$ with $\dur(\rho_7)=2$ where $Insulin$ is a reactant, and $Glycemia$ plays at the same time the role of inhibitor and product.

\begin{example}[Glucose metabolism -- reactions]\label{ex:glucosereac}
 The set of reactions $\RS = \{\rho_k=(R_k, I_k, P_k) \mid k\in [1..9]\}$ for the glucose metabolism example  is:
$$\begin{array}{l|c|c|c}
 \rho_k & Reactants \ R_k & Inhibitors \ I_k & Products \ P_k  \\
\hline
  \rho_1 \ & (Sugar,1) &\emptyset &(Insulin,+1), (Glycemia,+1) \\
  \hline
	\rho_2 & (Aspartame,1)& \emptyset &(Insulin,+1) \\
  \hline
	\rho_3 & \emptyset &(Glycemia,1)& (Glucagon,+1) \\
 % (\rho_4) & \{(Glycemia,1)\} &\{(Glycemia,2)\}& \{(NT,+)\} &1\\
 % (\rho_5) & \{(Glycemia,2)\} &\{(Glycemia,3)\}& \{(NT,-)\} &1\\
  \hline
	\rho_4 & (Glycemia,3)& \emptyset& (Insulin,+1) \\
  \hline
	\rho_5 & (Insulin,2) & \emptyset &(Glycemia,-1) \\
  \hline
	\rho_6 & (Insulin,1), &&\\
           & (Glycemia,3) & \emptyset &(Glycemia,-1) \\
  \hline
	\rho_7 & (Insulin,1) &  (Glycemia,2) &(Glycemia,-1) \\
  \hline
	\rho_{8} & (Glucagon,1) &\emptyset & (Glycemia,+1)  
   \end{array}
 $$
$\rho_1$ and $\rho_2$ represent the assimilation of Sugar and Aspartame, respectively: while Aspartame only increases the level of Insulin, Sugar also increases Glycemia.  $\rho_3$ takes care of hypoglycemia, \ie a Glycemia level equal to 0 (obtained by using $(Glycemia, 1)$ as inhibitor) engenders the production of Glucagon. On the contrary, hyperglycemia causes the production of Insulin ($\rho_4$). The presence of Insulin lowers Glycemia (reactions $\rho_5, \rho_6, \rho_7$). In particular Insulin level equal to 1 plays a role in the decrease of Glycemia only in case of hyperglycemia $\rho_6$ or hypoglycemia $\rho_7$, otherwise the signal is not strong enough and we need Insulin at level 2 to see the effect on Glycemia ($\rho_5$). Last reaction describes the role of Glucagon which if active increases the level of Glycemia.



\hfill $\diamond$
\end{example}


The dynamics of reaction networks is formalized using high-level Petri nets.  
We represent the state of a species $s$ as a pair $\tuple{\bool_s, \refr_s}$, 
where $\bool_s$ is an integer value storing  the current level from zero to $\setlev_s -1$,
and $\refr_s$ is a counter storing the interval of time spent at level $\bool_s$.  
The system is initialized by setting the level of all species: 
\ie  each species $s$ is set to $\tuple{\level{s}, 0} $ where $\level{s}$ is the given initial  level.

Reaction networks can evolve in two ways: 
\begin{enumerate}[{Case} 1.]

\item \label{item:clock} {\bf Time progression and Decay: } Time progresses discretely of one unit at once. It affects species with finite decay only. More precisely if a species $s$ has unbounded decay at level $\lev$ ($\life_s(\lev)=w$) then its corresponding tuple $(\level{s},\refr_s)$ remains unchanged. Otherwise, if the species has a finite decay ($\life_s(\lev)=d$), it may stay at level $\lev$ for $d$ time units. Then, degradation happens as soon as $d$ time units are elapsed and is obtained by decreasing the level to $\lev -1$ and by setting $\refr_s$ to zero.

\item  \label{item:reaction} {\bf Reaction: }A reaction $\rho$ may happen if and only if all the reactants are available at least at the required  level and all the inhibitors are expressed at a level strictly inferior to the required one. The triggering of a reaction results in the update  of the  level of all its products. Depending on the reaction, levels will be increased (+n) , maintained (0) or decreased (-n). 
We assume that each reaction can take place only once per time unit.


\end{enumerate}

We now comment on some specific design choices concerning reactions:
\begin{itemize}
 \item the set of reactants and inhibitors $R \cup I $ is allowed to be empty. This accounts for modeling an environment that is continuously sustaining the production of a species. 
%In this case the response time is ignored because not significant;  
 \item a species can appear in the same reaction simultaneously as a reactant and an inhibitor. In such a case, we require them to occur with  different levels: 
$$(\{(s,\level{})\} \cup R, \{(s, \level{}')\} \cup I , P )$$
where $\level{}< \level{}'$. This means that the reaction  can take place only if the level $\lev_s$ of $s$ belongs to the interval $\level{} \leq \lev_s < \level{}'$. In particular, if $s$ has to be present  in a reaction exactly at level $\level{}$, $s$ should appear as a reactant at level $\level{}$ %(that has to be present at least at level $\level{}$) 
and as inhibitor at level $\level{}'=\level{}+1$;% (that has to be at least at level strictly less than $\level{}+1$).
 \item  species can appear only once in the set of products $P$. This implies that a product cannot be increased and decreased in the same reaction.
\end{itemize}

It is also worth observing that if a species is continuously sustained  by some reactions then it remains available in the system at a certain  level for a period that could be longer than the corresponding decay time.  


\begin{example}[Glucose metabolism -- scenario]\label{ex:glucose_scenario}
Take once again the example of glucose metabolism and observe the behavior of
$Glycemia$ in the following scenario:
$$
\begin{array}{ll}
 \text{initial state} & \tuple{3, 0}  \\
 \text{$8$ time units elapse, counter at level $3$ updates} & \tuple{3, 8} \\
 \text{one time unit elapses, $Glycemia$ decays} & \tuple{2, 0} \\
  \text{one time unit elapses, counter at level $2$ updates} & \tuple{2, 1}\\
  \text{reaction $\rho_5$ decreases $Glycemia$ level} & \tuple{1, 0} \\
  \text{$8$ time units elapse, counter at level $1$ updates} & \tuple{1, 8} \\
\text{one time unit elapses, $Glycemia$ decays} & \tuple{0, 0}\\
  \text{one time unit elapses, no effect since $\life_{glycemia}(0)=\omega$ \quad} & \tuple{0, 0}. \qquad \diamond
\end{array}
$$
\end{example}


More formally, we now introduce the high-level Petri net modeling. 
Each species $s\in \res$ is modeled by a single place $q_s $ whose type   
$L(q_s)$ is the set of  tuples of the form  $\tuple{\lev_s, \refr_s}$, 
where $\lev_s \in [0..\setlev_s-1]$ and $\refr_s \in [0..max_s]$, %$\refr_s \in \nat$.
with $\mathit{max}_s=\mathsf{max}\{\life_s(l) \mid \life_s(l)\neq \omega \text{ and } l\in [0..\setlev_s-1] \}$.
In order to cope with time aspects we introduce a transition $t_c$ (Figure \ref{fig:clock}) connected to all species that is responsible for time progression and  takes care of the decay of concerned species (as described in Case \ref{item:clock} above).  
Finally, every reaction $\rho$ is modeled with  a transition $t_{\rho}$ (Figure \ref{fig:reaction}). To each transition  $t_{\rho}$ we associate a special place $q_{\rho}$ that is used to ensure that the same reaction is not executed more than once in the same time unit.
More detailed explanations for each type of transition follow Definition \ref{def:rs}. \looseness=-1
 

\begin{figure}[htb]
\centering
\subfigure[Clock transition with only one place of each kind ($q_s$ for $s\in\res$ and $q_\rho$ for $\rho\in\RS$). \label{fig:clock}]{
\begin{tikzpicture}[xscale=1.2, yscale=1.2, node distance=1.5cm,>=stealth',bend angle=20,auto]

  \node [place, label = right: $q_{\rho}$, label = above: $\vdots$,label = below: $\vdots$] at (3.5,0) (Pc){};
  \node [place, label=left:$q_s$,label = above: $\vdots$,label = below: $\vdots$]at (0,0)  (R){};

  \node [transition] (tC) at (2,0) {$t_{c}$}
   edge [pre,bend left]    node[above] {$w_{\rho}$}    (Pc)
   edge [post,bend right]   node[below]{$1$}    (Pc)
   edge [pre,bend right]    node[above] {$\tuple{\bool_s,\refr_s}$}    (R)
   edge [post,bend left]    node[auto] {$\tuple{\bool_s',\refr_s'}$}    (R);
  \node at (0,-1.5) (Z){};
\end{tikzpicture}
} \quad 
\subfigure[Transition for reaction $\rho= (R, I, P)$ with one place of each kind ($q_\rho, q_r$ for $r\in R$, $q_i$ for $i\in I$, $q_p$ for $p\in P$). \label{fig:reaction}]{
\begin{tikzpicture}[xscale=1.1, yscale=1.1, node distance=1.5cm,>=stealth',bend angle=20,auto]

 \node [place, label = right: $q_p$,label = left: $\cdots$] at (0,-1.5) (P){};
 %\node [place, label = above: $\Pclock$] at (0,2) (Pc){};
 \node [place, label = below: $q_r$,label = above: $\vdots$] at (-2,0) (R){};
 \node [place, label = below: $q_i$,label = above: $\vdots$] at (2,0) (I){};
 \node [place, label = right: $q_{\rho}$] at (0,1.5) (qw){};
 
 \node [transition] at (0,0) (tr) {$t_{\rho}$}
  % edge [pre and post]    node[above] {$z$}    (Pc)
   edge [pre and post]    node[above] {$\tuple{\bool_r,\refr_{r}}$}   (R)
   edge [pre and post]    node[above] {$\tuple{\bool_i,\refr_{i}}$}     (I)
   edge [pre, bend right]    node[left] {$\tuple{\bool_p,\refr_{p}}$}   (P)
   edge [post, bend left]   node[right] {$\tuple{\lev'_p,\refr'_p}$}     (P)
   edge [pre, bend left]    node[left] {$w_{\rho}$}   (qw)
   edge [post, bend right]   node[right] {$0$}     (qw);
   
\end{tikzpicture}
}
\caption{Scheme of Petri net modeling of reaction networks.}
\end{figure}



\begin{definition}\label{def:rs}
 Given a  network $(\res, \RS)$ with initial state $(s, \level{s})$ for each $s \in \res$,  its  high-level Petri net representation is defined as  tuple $(Q, T, F, L, M_0)$ where $z, z', \lev, \lev', \refr, \refr', w, w'$ are variables and:
\begin{itemize} 
 \item $Q =  \{q_s \mid  s \in{\res}\} \cup \{q_{\rho} \mid  \rho \in \RS \}; $
 \item $T= \{t_c \} \cup \{t_{\rho} \mid \rho \in \RS \}$;

 \item 
$  F=  \{ (q,t_c),(t_c, q) \mid q \in Q \} \quad  \cup$ \\
 \hspace*{0.63cm} $ \{ (q_s,t_{\rho}),(t_{\rho}, q_s), (q_{\rho},t_{\rho}),(t_{\rho}, q_{\rho}) \mid \rho \in \RS, s \in R_{\rho} \cup I_{\rho} \cup P_{\rho} \} 
$

 \item Labels for places in $Q$: 
$$
\begin{array}{c}

  L(q_{\rho})  = \{0,1\}  \text{ for each } \rho \in \RS  \\
L(q_s) = [0..\setlev_s-1] \times [0..\mathit{max}_s]   \text{ for each } s \in \res 
\end{array}
$$

\item Labels for arcs in $F$:
$$
\begin{array}{llr}
 L((q_{\rho}, t_c)) = w & L((t_c, \Pclock )) = 1\\
    L((q_s, t_c)) = \tuple{\bool_s, \refr_s} & L((t_c, q_s)) = \tuple{\bool_s', \refr_s'} & \text{ for each } s\in \res
\end{array}
$$
For each reaction $\rho  \in \RS$ and $s \in R_{\rho} \cup I_{\rho} \cup P_{\rho}$:
$$
\begin{array}{llr}
     L((q_s, t_{\rho})) = \tuple{\bool_s, \refr_s} \quad & %& L((t_{\rho}, q_s)) = \tuple{\bool_s, \refr_s, \birth_s} & \text{ for each } s\in R_{\rho}\cup I_{\rho},\\
     L((t_{\rho}, q_s)) = \begin{cases}
                           \tuple{\bool_s, \refr_s} & \text{if } s\notin P_{\rho}\\
                           \tuple{\bool_s', \refr_s'} & \text{otherwise}
                          \end{cases}\\
 
 %    L((q_p, t_{\rho})) = \tuple{\bool_p, \refr_p, \birth_p} & L((t_{\rho}, q_p)) = \tuple{\bool_p', \refr_p', \birth_p'} &  \text{ for each } p \in  P_{\rho},\\
     L((q_{\rho}, t_{\rho})) = w & L((t_{\rho}, q_{\rho} )) = 0
\end{array}
$$



\item Labels for transitions in $T$:
 $$
\begin{array}{lcl}
 L(t_c) &= &  \bigwedge_{s \in \res} \big(  ( \life(\lev_s) = \omega \vee  \refr_s+1 \leq \life(\lev_s)) \rightarrow \tuple{\lev'_s, \refr'_s} = \tuple{\lev_s, \refr_s+1}  \quad \wedge \\            
&& \hspace{1.1cm}( \life(\lev_s) \neq \omega  \wedge \refr_s+1 > \life(\lev_s)) \rightarrow  \tuple{\lev'_s, \refr'_s} = \tuple{\lev_s-1, 0} \big).
\end{array}
 $$

For each reaction $\rho  \in \RS$:
 $$
\begin{array}{lcl}
L(t_{\rho}) \! &=&   (w=1)  \wedge \bigwedge_{(r, \level{r}) \in R_{\rho}}(\lev_r \geq \level{r} )  \wedge   \bigwedge_{(i, \level{i}) \in I_{\rho}}(\lev_i < \level{i} )  \quad  \wedge \\
&& \bigwedge_{(p,z) \in P_{\rho}} (\tuple{\lev'_p, \refr'_p} = \tuple{\max(0,\min(\lev_p+ z, \setlev_p -1)),  0} 
\end{array}
 $$

 

\item For each $q\in Q$, $s\in \res$ and $\rho\in \RS$, the initial marking $M_0$ is:
$$
M_0(q) =
\begin{cases}
 1 & \text{if } q = q_{\rho}, \\
 \tuple{\level{s},0}& \text{if } q = q_s.
\end{cases}
$$
\end{itemize}

\end{definition}


We now comment on the transitions of the high-level Petri net. The result of the firing of a transition is handled by  guards (namely transition labels $L(t_c)$ and $L(t_{\rho})$) together with the evaluation $\sigma$ as described after Definition \ref{def:PTS}.   With an abuse of notation, in the following, we refer to evaluated variables without effectively mentioning the evaluation $\sigma$: \ie we say that the current value of the token in $q_{\rho}$ is $w$ instead of $\sigma(w)$.
Input and output arcs between the same place and transition with the same label (read arcs) are denoted in figures with a double-pointed arrow with a single label.


Clock transition $t_c$, depicted in Figure \ref{fig:clock}, takes care of Case \ref{item:clock} above. $t_c$ is responsible for  the decay of concerned species and the related update of counters $u_s$ of each species.
Moreover $t_c$ updates the tokens of all places $q_{\rho}$ to 1, thus re-enabling the possibility of performing a reaction $\rho$.


Next, we describe transitions for reactions, depicted in Figure \ref{fig:reaction}. Given a reaction $\rho=(R,I,P)$ we detail the conditions and the results of firing of $t_{\rho}$. As described in Case \ref{item:reaction} we have:
\begin{itemize}
 \item each reactant $r \in R$ has to be present at least at  level $\level{r}$,  this is expressed by  guard $\lev_r \geq \level{r}$; 
 \item each inhibitor $i\in I$ has not to exceed  level $\level{i}$,  this is guaranteed by guard 
$(\lev_i < \level{i})$;
\item each product $p \in P $  corresponding to place $q_p$ is updated to $ \tuple{\lev'_p, \refr'_p} =\tuple{\max(0,\min(\lev_p+ z, \setlev_p -1)),  0} $. 
\end{itemize}
The role of place $q_{\rho}$ is to forbid two consecutive executions of the same reaction in the same time unit.
Initially, the marking of $q_\rho$ is set to $1$ and it becomes $0$ when the transition $t_\rho$ is fired; 
then clock transition $t_c$ sets it to $1$ again.

Observe that, because of the semantics of high level Petri nets, reaction may not occur even if all constraints are satisfied. This is interpreted as the action of an hostile (non-specified) environment (e.g., reactants are too far from each other to react).



\begin{example}[Glucose metabolism -- reaction network]
\begin{figure}[ht]
\centering
\begin{tikzpicture}[xscale=1.2, yscale=1.3, node distance=1.5cm,>=stealth',bend angle=45,auto]

\tikzstyle{place}=[rectangle,rounded corners,draw,fill=blue!20,minimum size=7mm]


 \node [place, label = above: ] at (2,7) (sugar){$Sugar$};
 \node [place, label = above: ] at (6,7) (asp){$Aspartame$};
 \node [place, label = right: ] at (2,4) (glucose){$Glycemia$};
% \node [place, label = right: ] at (5,5) (nt){$Neurotransmitter$};
 %\node [place, label = left: ] at (0,2) (glycog){$Glycogenesis$};
% \node [place, label = right: ] at (4,2) (glycol){$Glycogenolysis$};
 \node [place, label = right: ] at (-2,4) (gluc){$Glucagon$}; 
 \node [place, label = right: ] at (6,4) (ins){$Insulin$}; 
 %\node [place, label = above: ] at (-1,5) (hunger){$Hunger$};
%\node [place, label = below: ] at (6,5) (clock){$Clock$};

\node [transition, label={[red] right:}] at (2,5.5) (tr1) {1}
  edge [pre]    node[left] {R}    (sugar)
  edge [ post]    node[above] {+}   (ins)
  edge [ post]    node[left] {+}   (glucose);
  
\node [transition, label={[red] right:}] at (6,5.5) (tr2) {2}
  edge [pre]    node[left] {R}    (asp)
  edge [post]    node[left] {+}   (ins);

  
  \node [transition, label={[red] right:}] at (0,4) (tr3) {3}
  edge [pre]    node[above] {I}    (glucose)
  edge [ post]    node[above] {+}   (gluc);
  
  
\node [transition, label={[red] right:}] at (4,4) (tr4) {4}
  edge [pre]    node[above] {R}    (glucose)
  edge [post]    node[above] {+}   (ins);
  



 \node [transition, label={[red] right:}] at (4,3) (tr5) {5}
   edge [pre]    node[above] {R}    (ins)
   edge [post]    node[above] {-}   (glucose);
   
   \node [transition, label={[red] right:}] at (4,2) (tr6) {6}
   edge [pre]    node[above] {R}    (glucose)
   edge [pre]    node[above] {R}    (ins)
   edge [post, bend left=30]    node[above] {-}   (glucose);
 

\node [transition, label={[red] right:}] at (4,1) (tr7) {7}
  edge [pre, bend left=35]    node[above] {I}    (glucose)
  edge [pre]    node[right] {R}    (ins)

  edge [post, bend left =60]    node[left] {-}   (glucose);

 
 \node [transition, label={[red] right:}] at (0,3) (tr8) {8}
  edge [pre]    node[below] {R}    (gluc)
  edge [post]    node[below] {+}   (glucose);

\end{tikzpicture}
 \caption{Simplified reaction network of glucose metabolism. } \label{fig:randyglucose}
\end{figure}


Figure \ref{fig:randyglucose} shows a simplification of the reaction network $(\res, \RS)$ given in example \ref{ex:glucose}. It focuses only on the reaction schema linking inputs (\ie reactants and inhibitors) to products. 
Each input arc is labeled with either  letter R or letter I denoting whether the input place is a reactant or an inhibitor,  respectively. Likewise, each output arc is labeled with a + or a - to denote increase or decrease of product levels by 1.
For each reaction transition $\rho$, we have omitted place $q_{\rho}$ and all arcs in the opposite direction. 
The numbers inside each transition refers to the corresponding reaction in Example \ref{ex:glucosereac}.

\begin{figure}[ht]
\centering
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

 \tikzstyle{place}=[circle,rounded corners, draw,fill=blue!30,minimum size=7mm]
 \tikzstyle{transition}=[rectangle,thick,draw=black!75,
 			 fill=black!20,minimum size=4mm]
 \tikzstyle{every token}=[font=\small]

% \node [place, label = right: $Glycogenesis$] at (3,-1) (glycog){};
 \node [place, label = above:$q_{glycemia}$ ] at (0,4) (gl){$(3,0)$}; 
 \node [place, label = below: $q_{insulin}$ ] at (0,0) (ins){$(0,0)$}; 
 %\node [place, label = below:$\qquad \ \Pclock$ ] at (0,2) (clock){};
 \node [place, label = right:$q_{\rho_7}$ ] at (6,2) (qw){1};
 
\node [transition, label={[red] left:$L(t_c)$} ] at (-3,2) (tr1) {$t_c$}
  %edge [post,bend left=30]    node[below] {$z'$}    (clock)
  %edge [pre ]    node[below] {$z$}    (clock)
  edge [pre, bend left]    node[left] {\ $\quad \tuple{\lev_{g},\refr_{g}}$}    (gl)
  edge [post]    node[right] {$\tuple{\lev'_{g},\refr'_{g}}$}    (gl)
  edge [pre, bend right ]    node [left] { $\tuple{\lev_i,\refr_i}$ }    (ins)
  edge [post ]    node[right] {$\ \tuple{\lev'_i,\refr'_i}$ }    (ins);
  
\node [transition, label={[red] right:$L(t_{\rho_7})$}] at (3,2) (tr8) {$t_{\rho_7}$}
  edge [pre, bend left=30 ]    node[above] {\qquad \quad $\tuple{\lev_g,\refr_g}$}    (gl)
  edge [pre and post]    node[right] {$\ \tuple{\lev_i,\refr_i}$}    (ins)
  %edge [pre and post]    node[below] {$z$}    (clock)
  edge [post,bend right]    node[right] {
  $ \tuple{\lev'_{g},\refr'_{g}} $}   (gl)
    edge [pre, bend left]    node[below] {$w$}   (qw)
  edge [post,bend right]    node[above] {$0$}   (qw);
\end{tikzpicture}
 \caption{A portion of the reaction network of glucose metabolism with an initial marking. } \label{fig:zoomrandyglucose}
\end{figure}


Figure \ref{fig:zoomrandyglucose}, instead, shows a portion of the complete 
initially marked reaction network for the glucose metabolism example, focusing only on reaction $\rho_7$. 
\hfill $\diamond$
\end{example}


From the above definition and the transition rule of high-level nets, 
we have the following properties: 
\begin{proposition}
Given a reaction network $(\res,\RS)$ with initial values $\level{s}$ for each species $s\in\res$: 
\begin{itemize}
	\item its Petri net representation has a finite structure with $|\res|+|\RS|$ places, $|\RS|+1$ transitions and the number of arcs is bounded by 
	$2(|\res|+|\RS|+\Sigma_{\rho=(R_\rho,I_\rho,P_\rho)\in\RS} (|R_\rho| + |I_\rho| + |P_\rho| + 1)$;
	\item each place type is a finite set;
	\item for each arc $(q,t)\in F$ there is an arc in opposite direction, \ie $(t,q)\in F$ and each arc label is a singleton;
	\item the initial marking and all reachable markings have exactly one structured token per place;
	\item the number of all reachable markings from the initial one is finite. 
\end{itemize}
 
\end{proposition}
\begin{proof}
Follows by definition and by induction on the length of a firing sequence. \qed
\end{proof}




\section{Toxicology analysis}\label{sec:toxic}

Such a Petri net representation of a reaction network is used to detect and predict toxic behaviors related to the  dynamics of bio-molecular networks. In order to verify toxicology properties, we resort to temporal logics and model checking techniques \cite{edmund}. For the sake of the present paper computation tree logic (CTL) allows to express properties of interest. Nonetheless different scenarios may require other more appropriate modal logic which we  could be  handled by our framework.

We recall here the basic concepts of CTL, provide the formal definition of the syntax and give some intuitions on the semantics, formally defined in \cite{emerson}.

A CTL formula is defined as: 
$$
\begin{array}{ll}
 \varphi::= &\bot \mid a \mid \neg \varphi \mid \varphi \vee \varphi \mid \varphi \wedge \varphi \mid \varphi \rightarrow \varphi \\
 & \esiste \x \varphi \mid \esiste \globally \varphi \mid \esiste (\varphi  \until \varphi) \mid \esiste \finally \varphi \mid \all \globally \varphi \mid \all \finally \varphi
\end{array}
 $$
where $a \in A$ is an atomic proposition.

CTL is used to state properties on branching time structures. %: its formulae refers to multiple runs at the same time.
It uses usual boolean operators, path quantifiers and temporal operators. Path quantifiers can be of two kinds: $\all \varphi$ means  that $\varphi$ has to hold on all paths starting from the current state, while $\esiste \varphi$ stands for there exists at least one path starting from the current state where $\varphi$ holds.
We have four temporal operators:  
$\x \varphi$ holds if $\varphi$ is true at the \emph{next} state, 
$\globally \varphi$ means that $\varphi$ has to \emph{globally} hold on the entire subsequent path, 
$\finally \varphi$ stands for eventually (or \emph{finally}) $\varphi$ has to hold (at some point on the subsequent path),
and $\varphi_1 \until \varphi_2$ means that $\varphi_1$ has to hold at least \emph{until} at some position $\varphi_2$ holds. 
In our context atomic formulae are represented by pairs of species and levels: $A = \{(s, \level{s}) \mid  s\in \res\}$, for instance $(Glucose,2)$.

As mentioned in the introduction, we are mainly interested in checking whether the inner equilibrium of an organism (tissue, cell, \dots) is maintained when administrating drugs or applying stressors.  More in detail, toxicology properties can be classified into two categories: 
\begin{itemize}
	\item properties  checking for the appearance  of particular symptoms, and
	\item properties characterizing causal relations between events.
\end{itemize}
The former class of properties basically consists in verifying reachability of some states, 
while the latter  concerns pathways that highlight sequences of events leading to toxic outcomes.
For instance, in the case of glucose regulation, we could verify whether glycemia levels are kept stable and whether they change in  case of ingestion of aspartame. More precisely, we could examine the causes and the symptoms of the hypoglycemia induced by the assimilation of aspartame. Hence  hypoglycemia is treated as a toxic state. 


\begin{example}[Glucose metabolism -- properties]
Take our running example of blood glucose regulation. The following properties can be expressed in CTL:

\begin{description}
 \item[Symptoms:] Is it possible to have an anomalous decrease of glucose levels in blood (revealing hypoglycemia)? 
$$\esiste \finally (Glycemia, 0)$$
 \item [Mode-of-action:] Recalling that the blood glucose regulation process normally maintains  glycemia at equilibrium (level $2$), is there an abnormal behavior leading to hypoglycemia?
$$\esiste (\esiste \finally (Glycemia, 2) ~\until~ (\esiste \finally (Glycemia, 0)))$$
 \item [Causality:] Does assimilation of sweeteners cause hypoglycemia? 
$$\begin{array}{l}
\esiste \finally [((Sugar, 1) \vee (Aspartame, 1)) \wedge (Glycemia, 1)] \rightarrow  \all \finally (Glycemia,2)   
  \end{array}
 $$
\end{description}

For the third formula we  show two paths given as sequences of reactions (abstracting away from time transitions), one that satisfy the formula and the other that contradicts it.
The first one corresponds to the assimilation of sugar. As described in Section \ref{sec:example}, the digestion of sugar induces an increase of the production of insulin and an augmentation of the blood glucose levels. Nonetheless the levels of insulin produced are not enough to cause the glycemia to drop and the formula is satisfied.
$$
\begin{array}{l}
(Sugar, 1), (Aspartame, 0), (Glycemia, 1), (Insulin, 0), (Glucagon, 0) \xrightarrow{\rho_1}\\
(Sugar, 1), (Aspartame, 0), \mathbf{(Glycemia, 2)}, (Insulin, 1), (Glucagon, 0) 
\end{array}
 $$
 
Unlike previous path, the assimilation of aspartame causes only an increase of insulin. Unfortunately, this increment is sufficient to induce a decrease of blood glucose levels thus contradicting the formula above.
$$
\begin{array}{l}
 (Sugar, 0), (Aspartame, 1), (Glycemia, 1), (Insulin, 0), (Glucagon, 0) \xrightarrow{\rho_2} \\ 
 (Sugar, 0), (Aspartame, 1), (Glycemia, 1), (Insulin, 1), (Glucagon, 0) \xrightarrow{\rho_7} \\
 (Sugar, 0), (Aspartame, 0), \mathbf{(Glycemia, 0)}, (Insulin, 1), (Glucagon, 0)
\end{array}
 $$
This illustrates the toxic behavior caused by aspartame described in Section \ref{sec:example}. 

\hfill $\diamond$
\end{example}

\section{Related work}

The main application of our work concerns the verification of properties of systems defined in terms of rules or reactions. 
From a technical point of view, the closest related work is on reaction systems \cite{DBLP:journals/ijfcs/BrijderEMR11} or their Petri net representation \cite{koutnyreaction}. Although we use a similar definition for reactions, the semantics that we have proposed is inherently different: in \cite{DBLP:journals/ijfcs/BrijderEMR11}  all  enabled reactions occur in one step while we have considered an interleaving semantics. 
In  \cite{DBLP:conf/birthday/BrijderER11}, the authors consider an extension of reaction systems with a notion of decay, this concept is different from the one considered here as we refer to an independent time progression while they count the number of  maximally concurrent steps. 
In fact, our representation of time is considerably different from the approaches traditionally used in time and timed Petri nets 
(\cite{DBLP:journals/tcs/CeroneM99} presents a survey with insightful comparison of the different approaches).
The main difference lies on the fact that the  progression of time is implicit and  external to the system. By contrast, in our proposal we have assumed the presence of  an explicit way of incrementing durations (modeled by synchronized counters). 
This is also  different from the notion of timestamps introduced in  \cite{timestamp} that again refers to an implicit notion of time.
Indeed,  our approach is conceptually closer to Petri nets with causal time  \cite{DBLP:journals/entcs/ThanhKP02} for the presence of an explicit transition for time progression. Nevertheless, in reaction networks time cannot be suspended under the influence of the environment (as is the case in \cite{DBLP:journals/entcs/ThanhKP02}).
 
In a broader sense, our work could also be related to P-systems \cite{DBLP:journals/ijfcs/PaunPRS11,DBLP:journals/fuin/KleijnK11} or the $\kappa$-calculus \cite{DBLP:journals/tcs/DanosL04} that  describe the evolution of cells through rules. 
Both these approaches are mainly oriented to simulation while we are interested in  verification aspects. Finally, always related to the modeling in Petri nets but with a different aim,  levels have been used in qualitative approaches to address problems related to the identification of steady states in genetic networks such as in \cite{DBLP:journals/nc/ChaouiyaNRT11}.  Nevertheless these contributions abstract away from time related aspects that are instead central in our proposal. 

\section{Conclusion and future work}
\label{sec:concl}
We have introduced a high-level Petri net modeling of reaction networks to address problems related to toxicogenomics. In reaction networks, systems consist of a set of species present in the environment at a given level. Species can degrade with time progression and their presence is governed by a set of rules (reactions). In a reaction, species can have the role of reactants, inhibitors or products. A reaction can take place only if all reactants are available and all  inhibitors are not. Depending on the type of reaction, products  levels are either increased or decreased. We have shown that properties of biological systems can be expressed in a suitable temporal logic and verified on the finite state space of the network.  
We have illustrated our framework  in the modeling of blood glucose regulation. 

We are currently investigating how to enrich reactions with response time, representing the required time for yielding products \cite{techrep}. This poses new questions on how our model with time constraints could be compared to other existing time concepts 
for instance that in timed automata or that in stochastic models like in \cite{DBLP:conf/sfm/HeinerGD08,DBLP:conf/apn/GilbertHLS13}.

% <<<<<<< .mine
% Finally, our model is currently being implemented thanks to  Snakes \cite{Pom-PNN-2008} library. Formulae can be checked via the  Neko  tool \cite{FP-PNSE-2013} developed in conjunction with Snakes 
% =======
Finally, we have a prototype implemented with Snakes \cite{Pom-PNN-2008} and we plan to use Snoopy \cite{DBLP:conf/apn/HeinerHLRS12} and connected tools (Marcie \cite{DBLP:conf/qest/SchwarickHR11}) to simulate and analyze CTL formulae.  



\subsubsection*{Acknowledgments.}
We would like to thank Michel Malo and the anonymous reviewers for their comments and insightful suggestions.
This work was supported by the French project ANR BLANC 0307 01 - SYNBIOTIC.
 

\bibliographystyle{abbrv}
\bibliography{biblio}



 


\end{document}
